(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
(declare-const r Float32)
(assert (= x (fp #b0 #b01111111 #b00101111011101100110001)))
(assert (= y (fp #b0 #b01111111 #b11110000011000001011001)))
(assert (= z (fp #b0 #b01100110 #b01110101110111111011001)))
(assert (= r (fp #b0 #b10000000 #b00100110001100111111111)))
(assert (not (= (fp.fma RNE x y z) r)))
(check-sat)
